parameter ADDR = 16;
parameter DATA = 8;
parameter BLOC = 3;

module AsyncMem ( 
  input clock, reset,

  output logic                             allocReady,
  input  logic                             allocValid,
  
  input  logic [ADDR - 1:0]                allocAddr,
  output logic [DATA * (1 << BLOC) - 1:0]  allocData,

  output logic                             writeReady,
  input  logic                             writeValid,
  
  input  logic [ADDR - 1:0]                writeAddr,
  input  logic [DATA * (1 << BLOC) - 1:0]  writeData
);

  logic [DATA - 1:0] regs [1 << ADDR];

  always_comb begin 
    if (reset) begin
      writeReady = 1'b0;
      allocReady = 1'b0;
    end else begin
      writeReady = 1'b1;
      allocReady = 1'b1;
    end

    for (integer bloc = 0; bloc < (1 << BLOC); bloc += 1)
      allocData[bloc * DATA +: DATA] <= regs[allocAddr + bloc];

  end

  always_ff @(posedge clock) begin
    if (writeValid) for (integer bloc = 0; bloc < (1 << BLOC); bloc += 1)
      regs[writeAddr + bloc] <= writeData[bloc * DATA +: DATA];
  end

`ifdef FORMAL

  logic epoch = 1'b0;
  
  (* anyconst *) logic [ADDR - 1: 0] addr_form;

  always @(posedge clock) begin

    if (reset) 
      RESET: assert(!writeReady && !allocReady);

    if ($fell(reset)) epoch <= 1'b1;

    // The Properties of Memory:
    // =========================
    //
    // 1. `alloc_valid` is not effected since there is no more logic between regs
    //    and output. 
    //
    // 2. `alloc_ready` will be supressed by `write_valid` signal.
    //
    // 3. `write_valid` effects at CURR CYCLE; the action of saving carries on at 
    //    NEXT POS EDGE. The latest written data can be read in the NEXT CYCLE.
    //
    // 4. Properties w.r.t. Memory Persistence 
    // 
    // 4.1. The data writed in particular `addr_write` will remain UNTIL next write
    //      request. (this one is subtle, and hard to describe formally)
    // 
    // 4.2. The data writed in particular address OTHER THAN `addr_write` will not
    //      affected by the write request with `addr_write`.

    if (epoch && $stable(epoch)) begin
      if (addr_form == allocAddr)
        
        // MEM_PROP_1: assert(allocData == {>>{regs[allocAddr +: (1 << BLOC)]}});
        
        for (integer bloc = 0; bloc < (1 << BLOC); bloc += 1)
          assert(allocData[bloc * DATA +: DATA] == regs[allocAddr + bloc]);             

      if ($past(writeValid) && $past(addr_form == writeAddr)) begin

        // MEM_PROP_2: assert(!$past(allocReady));
        // MEM_PROP_3: assert({>>{regs[writeAddr +: (1 << BLOC)]}} == $past(writeData));

        for (integer bloc = 0; bloc < (1 << BLOC); bloc += 1)
          assert($past(writeData[bloc * DATA +: DATA]) == regs[$past(writeAddr) + bloc]);   
      
      end

      if (!$past(writeValid)) begin
        MEM_PROP_4_1: assert($stable(regs[$past(addr_form)]));
      end

      assume($past(writeAddr[BLOC-1:0]) == 0);
      if ($past(addr_form[ADDR-1:BLOC] != writeAddr[ADDR-1:BLOC]) && $stable($past(addr_form))) begin
        MEM_PROP_4_2: assert($stable(regs[$past(addr_form)]));
      end 

    end
  end

`endif


endmodule: AsyncMem
